format doc #1130
format doc #1130
Conversation
affeldt-aist
added
documentation 📝
| Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) := | ||
| {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}. |
There was a problem hiding this comment.
According to WP, this should rather be monotonic and I would expect it to be non strict (with homo instead of mono). Maybe we should also have a strict version. I would also expect it to use nondecreasing_fun and the like from realfun.v.
All in all, maybe this change should come in a separate PR so as to not delay the remaining of the current PR.
There was a problem hiding this comment.
Yes, I will issue about it to avoid mixing topics.
|
This CI failure is obviously unrelated (and a sign that we should really drop MC1 to avoid having to maintain two branches). |
Co-authored-by: Pierre Roux <[email protected]>
affeldt-aist
force-pushed
the
topology_20240202
branch
from
7b68f4f to
1cba8ff
Compare
|
The changes look good (sorry for reviewing after the merger). |
* format doc --------- Co-authored-by: Pierre Roux <[email protected]>
* format doc --------- Co-authored-by: Pierre Roux <[email protected]>
proux01
removed
the
TODO: MC2 port
Motivation for this change
The goal of this PR is to format the documentation of
topology.vto bring itone step closer to the format expected for the HB release (ideally, we should
only need to update locally a few subsections when moving it to HB).
Ref: https://github.com/math-comp/math-comp/wiki/How-to-document
Note that this will still need to be updated soon to fit the format of coq2html
(this will be taken care of when rebasing PR #1108 ).
It happens that this PR also fixes a few minor issues with the documentation
(that was not properly updated) and it restores the ordering
(identifiers appear in the documentation in an order close to the
order in which they appear in the file, this makes it easier to edit it now
and should make it easier to split the file in the future).
@t6s This is the first pass of the first pass we talked about during the last MathComp-Analysis dev meeting.
Things done/to do
CHANGELOG_UNRELEASED.mdCompatibility with MathComp 2.0
TODO: HB portto make sure someone ports this PR tothe
hierarchy-builderbranch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.